\documentclass[12pt]{article}
\usepackage[utf8]{inputenc}
\usepackage[russian]{babel}
\usepackage{cmap}
\usepackage[pdftex]{graphicx}
\usepackage{indentfirst}
\usepackage{enumitem}

\title{Распределение симметричных ключей}
\author{Н. Смарт}

\begin{document}
\maketitle
\section{Формальные методы проверки протоколов}
Из обсуждения протоколов в предыдущем параграфе можно сделать вывод, что они весьма запутаны, и выявление их недостатков является весьма тонким делом. Чтобы подойти к этой задаче с научной точки зрения, необходимо разобрать соответствующий аппарат. Наиболее сильный из них - \textit{BAN}-логика, изобретенная Барроузом, Абади и Нидхеймом.\\

\textit{BAN}-логика, как и любая формальная логика, имеет ряд недостатков, но она была в свое время очень полезна при проектировании и анализе протоколов распределения симметричных ключей типа Цербер и Нидхейма-Шредера. В настоящее время она вытеснена более сложной техникой и формальными методами, но сохраняет свое значение как с исторической, так и с учебной точек зрения.\\

Основная идея \textit{BAN}-логики состоит в том, что при анализе протоколов в первую очередь стоит обратить внимание на восприятие сторонами поступающей информации - что они принимают на веру, а что им доподлинно известно или может быть выведено логическим путем из достоверных для них фактов. Даже при современных подходах к моделированию инфраструктуры открытых ключей (\textit{PKI}) берут на вооружение эту идею, в связи с чем мы сейчас исследуем BAN-логику более подробно.\\

Введем обозначения.\\

\begin{itemize}
	\item[$\circ$] $P\mid \equiv Q$ $(P\:\mathsf{believes}\:Q)$ означает, что участник $P$ \textit{верит} в (или имеет право брать на веру) высказываение $X$, т.е. $P$ станет действовать так, как будто $X$ - истинная информация.
	\item[$\circ$] $P \triangleleft X$ $(P\:\mathsf{sees}\:Q)$подразумевает, что $P$ \textit{видит} $X$, т.е. кто-то послал сообщение пользователю $P$, в котором содержится $X$. Так что $P$ может прочесть и воспроизвести $X$.
	\item[$\circ$] $P\mid \sim Q$ $(P\:\mathsf{once\:said}\:Q)$ означает, что $P$ однажды высказал $X$ и в тот момент верил в его истинность. Заметим, что здесь мы не уточняем время этого события.
	\item[$\circ$] $P\mid \Rightarrow Q$ $(P\:\mathsf{has\:jurisdiction\:over}\:Q)$ означает, что $X$ входит в юрисдикцию $P$, т.е. $P$ обладает властью над $X$ и по этому вопросу $P$ можно доверять.
	\item[$\circ$] $\sharp X$ $(\mathsf{fresh}(X))$ означает, что высказывание $X$ получено недавно. Этот символ используется обычно для числовых вставок.
	\item[$\circ$]  $P \stackrel{k}{\longleftrightarrow} Q$ означает, что $P$ и $Q$ используют для общения \textit{разделенный
ключ} $k$. Предполагается, что ключ достаточно стоек и не может быть раскрыт никем из посторонних, если это не предусмотрено протоколом.
	\item[$\circ$] Обозначение $\lbrace X \rbrace_k$ обычно подразумевает, что данные $X$ зашифрованы ключом $k$. Шифрование считают совершенным, в частности $X$ остается зачекреченным до тех пор, пока одна из сторон сознательно не раскроет его в какой-то другой части протокола.
\end{itemize}

	Кроме того, вместо обычной операции <<И>> употребляется запятая, а запись  $\frac{A,B}{C}$ означает, что из истинности утверждений $A$ и $B$ следует истинность высказывания $C$. Такой способ символьного изображения сложных
конструкций принят во многих формальных логиках.\\

BAN-логика опирается на множество постулатов или правил вывода.
Мы разберем лишь главные из них.\\

\textit{Правило о значении сообщения:}\\

\begin{equation}
\frac{A\:\mathsf{believes}\:A \stackrel{K}{\longleftrightarrow} B, A\:\mathsf{sees}\:\lbrace X \rbrace_K}{A\:\mathsf{believes}\:B\:\mathsf{once\:said}\:X}
\end{equation}

Эквивалентная словесная формулировка: из предположений о том, что $A$ верит в совместное использование ключа $K$ с $B$, и $A$ видит сообщение $X$, зашифрованное ключом $K$, мы делаем вывод: $A$ верит, что $B$ в какой-то момент высказал $X$. Заметим, что здесь неявно предполагается, что сам $A$ никогда не высказывал $X$.\\

\textit{Правило проверки уникальности числовых вставок:}
\begin{equation}
\frac{A\:\mathsf{believes}\:\mathsf{fresh}(X), A\:\mathsf{believes}\:B\:\mathsf{once\:said}\:X}{A\:\mathsf{believes}\:B\:\mathsf{believes}\:X}
\end{equation}
т.е. если $A$ верит в новизну $X$ и в то, что $B$ когда-то высказал $X$, то $A$ верит, что $B$ по-прежнему доверяет $X$.\\

\textit{Правило юрисдикции:}
\begin{equation}
\frac{A\:\mathsf{believes}\:B\:\mathsf{has\:jurisdiction\:over}\:X, A\:\mathsf{believes}\:B\:\mathsf{believes}\:X}{A\:\mathsf{believes}\:X}
\end{equation}
говорит, что если $A$ верит в полномочия $B$ относительно $X$, т.е. $A$ полагается на $B$ в деле с $X$, и $A$ верит в то, что $B$ верит в $X$, то $A$ должен верить в $X$.\\

\textit{Другие правила.} Оператор доверия и запятая, разделяющая высказывания, рассматриваемые совместно, подчиняются следующим соотношениям:

\begin{equation}
\frac{P\:\mathsf{believes}\:X, P\:\mathsf{believes}\:Y}{P\:\mathsf{believes}\:(X,Y)}
\end{equation}

\begin{equation}
\frac{P\:\mathsf{believes}\:(X,Y)}{P\:\mathsf{believes}\:X}
\end{equation}

\begin{equation}
\frac{P\:\mathsf{believes}\:Q\:\mathsf{believes}\:(X,Y)}{P\:\mathsf{believes}\:Q\:\mathsf{believes}\:X}
\end{equation}

Оператор <<однажды высказал>> удовлетворяет аналогичному соотношению:
\begin{equation}
\frac{P\:\mathsf{believes}\:Q\:\mathsf{once\:said}\:(X,Y)}{P\:\mathsf{believes}\:Q\:\mathsf{once\:said}\:X}
\end{equation}

Заметим, что предположения $P\:\mathsf{believes}\:Q\:\mathsf{once\:said}\:X$ и $P\:\mathsf{believes}\:Q\:\mathsf{once\:said}\:Y$ не влекут утверждения $P\:\mathsf{believes}\:Q\:\mathsf{once\:said}\:(X,Y)$, поскольку последнее означает, что Q
произнес X и У в одно и то же время. Наконец, если какая-то часть высказывания получена недавно, то это же можно утверждать и про всю конструкцию:
\begin{equation}
\frac{P\:\mathsf{believes}\;\mathsf{fresh}\:X}{P\:\mathsf{believes}\;\mathsf{fresh}\:(X,Y)}
\end{equation}

Попытаемся теперь проанализировать протокол выбора ключа для $A$ и $B$, опираясь на \textit{BAN}-логику. Прежде всего сформулируем цели протокола, которые как минимум состоят в следующем:
\begin{equation}
A\:\mathsf{believes}\:A \stackrel{K}{\longleftrightarrow} B
\end{equation}
\begin{equation}
B\:\mathsf{believes}\:A \stackrel{K}{\longleftrightarrow} B
\end{equation}
т.е. оба участника должны поверить в то, что они нашли секретный ключ для обмена друг с другом закрытой информацией.\\

Однако можно было бы потребовать и большего, например,
\begin{equation}
A\:\mathsf{believes}\:B\:\mathsf{believes}\:A \stackrel{K}{\longleftrightarrow} B
\end{equation}
\begin{equation}
B\:\mathsf{believes}\:A\:\mathsf{believes}\:A \stackrel{K}{\longleftrightarrow} B
\end{equation}
что обычно называют подтверждением приема ключа. Иначе говоря, можно считать, что в результате работы протокола $A$ будет уверен в знании $B$ о том, что он разделяет секретный ключ с $A$, а $B$ верит в то, что и $A$ знает об их обшем ключе.\\

Перепишем протокол в символьной форме согласно правилам \textit{BAN}-логики. Этот процесс называется идеализацией и наиболее
уязвим для ошибок, поскольку его невозможно автоматизировать. Кроме того, нам необходимо сделать предположения или сформулировать постулаты, которые считаются истинными в начале работы протокола.\\

Для наглядности, чтобы понять, как это все работает <<в реальной жизни>>, подвергнем анализу протокол широкоротой лягушки,
использующий синхронизацию часов.\\

\section{Анализ протокола широкоротой лягушки}

Напомним, что он состоит из обмена двумя сообщениями:\\
\begin{equation}
A \longrightarrow S:A,\lbrace t_a,b,k_{ab} \rbrace_{k_{ab}}
\end{equation}
\begin{equation}
S \longrightarrow B:\lbrace t_s,a,k_{ab} \rbrace_{k_{bs}}
\end{equation}

При идеализации это выглядит так:
\begin{equation}
A \longrightarrow S: \lbrace t_a, A \stackrel{k_{ab}}{\longleftrightarrow} B \rbrace_{k_{as}}
\end{equation}
\begin{equation}
S \longrightarrow B: \lbrace t_s, A\:\mathsf{believes}\:A\stackrel{k_{ab}}{\longleftrightarrow} B \rbrace_{k_{bs}}
\end{equation}

Идеализированное первое сообщение говорит S, что\\
\begin{list}{-}{}
\item $t_a$ - временн\'{а}я или числовая вставка,
\item $k_{ab}$ - ключ, который прeдлагаeтся использовать для коммуникации с $B$.
\end{list}
Итак, какие предположения сделаны в начале работы протокола? Ясно, что $A$, $B$ и $S$ используют секретные ключи для обмена шифрованными сообщениями друг с другом, что на языке $BAN$-логики
может быть выражено как
\begin{equation}
A\:\mathsf{believes}\: A\stackrel{k_{as}}{\longleftrightarrow} S
\end{equation}
\begin{equation}
B\:\mathsf{believes}\: B\stackrel{k_{bs}}{\longleftrightarrow} S
\end{equation}
\begin{equation}
S\:\mathsf{believes}\: A\stackrel{k_{as}}{\longleftrightarrow} S
\end{equation}
\begin{equation}
B\:\mathsf{believes}\: A\stackrel{k_{bs}}{\longleftrightarrow} S
\end{equation}
Есть пара предположений о временн\'{ы}х вставках:
\begin{equation}
S \:\mathsf{believes}\: \mathsf{fresh}
\:t_a
\end{equation}
\begin{equation}
B \:\mathsf{believes}\: \mathsf{fresh
}\:t_s
\end{equation}
и еще три предположения:
\begin{list}{-}{}
\item $B$ полагается на $A$ в выборе хорошего ключа:
\begin{equation}
B \:\mathsf{believes}\: (A\:\mathsf{has\:jurisdiction\:over}A\stackrel{k_{ab}}{\longleftrightarrow} B)
\end{equation}
\item $B$ доверяет $S$ передать ключ от $A$:
\begin{equation}
B \:\mathsf{believes}\: (S\:\mathsf{has\:jurisdiction\:over}A \:\mathsf{believes}\:A\stackrel{k_{ab}}{\longleftrightarrow} B)
\end{equation}
\item $A$ верит, что сеансовый ключ принят:
\begin{equation}
A \:\mathsf{believes}\:A\stackrel{k_{ab}}{\longleftrightarrow} B
\end{equation}
\end{list}
Обратите внимание на то, как последние предположения обнажают проблемы, связанные с протоколом, о которых мы говорили ранее.\\

Опираясь на сделанные предположения, мы можем проанализировать протокол. Посмотрим, какой вывод можно сделать из первого сообщения $A \longrightarrow S:A,\lbrace t_a,b,k_{ab} \rbrace_{k_{ab}}$.
\begin{list}{-}{}
\item $S$, видя сообщение, зашифрованное ключом $k_{as}$, может сделать вывод о том, что оно послано клиентом $A$.
\item Наличие свежей временной вставки $t_a$ позволяет участнику $S$ заключить, что и все сообщение написано недавно.
\item Из свежести всего сообщения $S$ выводит, что клиент $A$ верил в то, что послал.
\item Следовательно,
\begin{equation}
S \:\mathsf{believes}\:A\:\mathsf{believes}\:A\stackrel{k_{ab}}{\longleftrightarrow} B
\end{equation}
т.е. $S$ подготовлен к посылке второго сообщения протокола.
\end{list}

Обратимся к следующему этапу: $S \longrightarrow B: \lbrace t_s, A\:\mathsf{believes}\:A\stackrel{k_{ab}}{\longleftrightarrow} B \rbrace_{k_{bs}}$
\begin{list}{-}{}
\item Увидев послание, зашифрованное ключом $k_{bs}$, клиент $В$ понимает,
что оно было отправлено $S$.
\item Временн\'{а}я вставка $t_s$ доказывает $B$, что все сообщение было
послано только что.
\item Ввиду свежести сообщения, $B$ заключает, что $S$ доверяет всему
посланному.
\item В частности, $B$ верит в то, что $S$ доверяет второй части сообщения.
\item Но $B$ верит и в то, что в юрисдикцию $S$ входит выяснить,
знает ли его партнер $А$ секретный ключ, и поэтому $B$ вверяет $A$ полномочия по генерированию ключа.
\end{list}
Из этих рассуждений можно сделать вывод:
\begin{equation}
B\:\mathsf{believes}\: A\stackrel{k_{ab}}{\longleftrightarrow} B
\end{equation}
\begin{equation}
B\:\mathsf{believes}\: A:\mathsf{believes}\:A\stackrel{k_{ab}}{\longleftrightarrow} B
\end{equation}
Комбинируя это с исходным предположением: $A\:\mathsf{believes}\: A\stackrel{k_{ab}}{\longleftrightarrow} B$, получаем, что анализируемый протокол распределения ключей обоснован. Единственное, чего мы не встретили в нем, это
\begin{equation}
A\:\mathsf{believes}\: B:\mathsf{believes}\:A\stackrel{k_{ab}}{\longleftrightarrow} B
\end{equation}
т. е. А не добился подтверждения тому, что В получил нужный ключ.\\
Обратите внимание на то, что применение BAN-логики к анализу формализовало все этапы протокола, так что их стало легче
сравнивать с предположениями, необходимыми любому протоколу для работы. Кроме того, этот формализм проясняет точки зрения на работу протокола всех его участников.
\end{document}
